// SPDX-License-Identifier: GPL-2.0 or GPL-3.0
// Copyright © 2019 Ariadne Devos

/* TODO: apparently, cmov was introduced in i686
  -- portable tissues */

/* Side-channel considerations: all passed values are not secret. */

/*  Operational semantics: If %0 > %1, do %0 <- %1.
  Functional semantics:

  In case \old(%0) >(*) \old(%1) (branch taken),
  - \old(%1) = min(\old(%0), \old(%1)) (case analysis)
  - \new(%0) = \old(%1) = min(\old(%0), \old(%1)) (assignment, previous lemma)
  Otherwise, the negation holds: \old(%0) <= \old(%1),
  - \old(%0) = min(\old(%0), \old(%1)) (case analysis)
  - \new(%0) = \old(%0) = min(\old(%0), \old(%1)) (no assignment, previous lemma)

  (*) '>=' also suffices.

  Therefore, \new(%0) = min(\old(%0), \old(%1)) (consider both branches)

  -- Assembly sequence

  The Intel / AT&T syntax differences in operand order are
  very confusing. Testing:

  Try "mov $0, %0". It compiles, so the first operand is the source,
  and the latter the destination. That proofs the second operand of
  "cmov??" is correct: it is %0, `*x_set_p` that must be updated.

  Another source of confusion is Intel's distinction between greater / less
  and above / below. The former is signed, the latter unsigned.

  To test: 2 (operand order of cmp) * 2 (above / below).
  Pass: %0,%1,below; %1,%0,above.
  (These two are equivalent: %0 < %1 <-> %1 > 0.
  Sanity check succeeds.)

  cc: condition code is changed by 'cmp'. */
#define _sHT_min(x_set_p, y) \
	__asm__("cmp %1,%0;cmova %1,%0" : "+r" (*(x_set_p)) : "r" (y) : "cc")
